Termination proof of /tmp/tmpuzQxmC/Shuffle.jar

Termination of the given JBC could be proven:

0 JBC

↳1 JBCToGraph (⇒, 520 ms)

↳2 JBCTerminationGraph

↳3 TerminationGraphToSCCProof (⇒, 0 ms)

↳4 AND

    ↳5 JBCTerminationSCC

        ↳6 SCCToIDPv1Proof (⇒, 130 ms)

        ↳7 IDP

        ↳8 IDPtoQDPProof (⇒, 20 ms)

        ↳9 QDP

        ↳10 QDPSizeChangeProof (⇔, 0 ms)

        ↳11 YES

    ↳12 JBCTerminationSCC

        ↳13 SCCToIDPv1Proof (⇒, 140 ms)

        ↳14 IDP

        ↳15 IDPNonInfProof (⇒, 110 ms)

        ↳16 AND

            ↳17 IDP

                ↳18 IDependencyGraphProof (⇔, 0 ms)

                ↳19 TRUE

            ↳20 IDP

                ↳21 IDependencyGraphProof (⇔, 0 ms)

                ↳22 TRUE

    ↳23 JBCTerminationSCC

        ↳24 SCCToIDPv1Proof (⇒, 1010 ms)

        ↳25 IDP

        ↳26 IDPtoQDPProof (⇒, 0 ms)

        ↳27 QDP

        ↳28 DependencyGraphProof (⇔, 0 ms)

        ↳29 QDP

        ↳30 MRRProof (⇔, 0 ms)

        ↳31 QDP

        ↳32 DependencyGraphProof (⇔, 0 ms)

        ↳33 TRUE

(0) Obligation:

JBC Problem based on JBC Program:
Manifest-Version: 1.0 Created-By: 1.6.0_16 (Sun Microsystems Inc.) Main-Class: Shuffle

public class Random {
  static String[] args;
  static int index = 0;

  public static int random() {
    String string = args[index];
    index++;
    return string.length();
  }
}


public class Shuffle{

  // adapted from [Walther, 94]
  public static void main(String[] args) {
    Random.args = args;
    IntList l = IntList.createIntList();
    IntList res = null;

    while (l != null) {

      res = new IntList(l.value, res);
      l = l.next;
      if (l != null) l = l.reverse();

    }

  }
}


class IntList {
  int value;
  IntList next;

  public IntList(int value, IntList next) {
    this.value = value;
    this.next = next;
  }


  public static IntList createIntList() {

    int i = Random.random();
    int j;

    IntList l = null;

    while (i > 0) {
      j = Random.random();
      l = new IntList(j, l);
      i--;
    }

    return l;
  }

  public IntList reverse() {

    IntList res = null;
    IntList l = this;

    while (l != null) {
      res = new IntList(l.value, res);
      l = l.next;

    }

    return res;
  }
}

(1) JBCToGraph (SOUND transformation)

Constructed TerminationGraph.

(2) Obligation:

Termination Graph based on JBC Program:
Shuffle.main([Ljava/lang/String;)V: Graph of 94 nodes with 1 SCC.

IntList.createIntList()LIntList;: Graph of 165 nodes with 1 SCC.

IntList.reverse()LIntList;: Graph of 54 nodes with 1 SCC.

(3) TerminationGraphToSCCProof (SOUND transformation)

Splitted TerminationGraph to 3 SCCss.

(4) Complex Obligation (AND)

(5) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: IntList.reverse()LIntList;
SCC calls the following helper methods:
Performed SCC analyses: UsedFieldsAnalysis

(6) SCCToIDPv1Proof (SOUND transformation)

Transformed FIGraph SCCs to IDPs. Log:

Generated 46 rules for P and 0 rules for R.

P rules:
1717_0_reverse_NULL(EOS(STATIC_1717), java.lang.Object(o828sub), java.lang.Object(o828sub)) → 1719_0_reverse_NULL(EOS(STATIC_1719), java.lang.Object(o828sub), java.lang.Object(o828sub))
1719_0_reverse_NULL(EOS(STATIC_1719), java.lang.Object(o828sub), java.lang.Object(o828sub)) → 1721_0_reverse_New(EOS(STATIC_1721), java.lang.Object(o828sub))
1721_0_reverse_New(EOS(STATIC_1721), java.lang.Object(o828sub)) → 1725_0_reverse_Duplicate(EOS(STATIC_1725), java.lang.Object(o828sub))
1725_0_reverse_Duplicate(EOS(STATIC_1725), java.lang.Object(o828sub)) → 1728_0_reverse_Load(EOS(STATIC_1728), java.lang.Object(o828sub))
1728_0_reverse_Load(EOS(STATIC_1728), java.lang.Object(o828sub)) → 1731_0_reverse_FieldAccess(EOS(STATIC_1731), java.lang.Object(o828sub), java.lang.Object(o828sub))
1731_0_reverse_FieldAccess(EOS(STATIC_1731), java.lang.Object(o828sub), java.lang.Object(o828sub)) → 1736_0_reverse_FieldAccess(EOS(STATIC_1736), java.lang.Object(o828sub), java.lang.Object(o828sub))
1731_0_reverse_FieldAccess(EOS(STATIC_1731), java.lang.Object(o815sub), java.lang.Object(o815sub)) → 1737_0_reverse_FieldAccess(EOS(STATIC_1737), java.lang.Object(o815sub), java.lang.Object(o815sub))
1736_0_reverse_FieldAccess(EOS(STATIC_1736), java.lang.Object(IntList(EOC, i487, o833)), java.lang.Object(IntList(EOC, i487, o833))) → 1740_0_reverse_FieldAccess(EOS(STATIC_1740), java.lang.Object(IntList(EOC, i487, o833)), java.lang.Object(IntList(EOC, i487, o833)))
1740_0_reverse_FieldAccess(EOS(STATIC_1740), java.lang.Object(IntList(EOC, i487, o833)), java.lang.Object(IntList(EOC, i487, o833))) → 1745_0_reverse_Load(EOS(STATIC_1745), java.lang.Object(IntList(EOC, i487, o833)))
1745_0_reverse_Load(EOS(STATIC_1745), java.lang.Object(IntList(EOC, i487, o833))) → 1750_0_reverse_InvokeMethod(EOS(STATIC_1750), java.lang.Object(IntList(EOC, i487, o833)))
1750_0_reverse_InvokeMethod(EOS(STATIC_1750), java.lang.Object(IntList(EOC, i487, o833))) → 1755_0_<init>_Load(EOS(STATIC_1755), java.lang.Object(IntList(EOC, i487, o833)))
1755_0_<init>_Load(EOS(STATIC_1755), java.lang.Object(IntList(EOC, i487, o833))) → 1758_0_<init>_InvokeMethod(EOS(STATIC_1758), java.lang.Object(IntList(EOC, i487, o833)))
1758_0_<init>_InvokeMethod(EOS(STATIC_1758), java.lang.Object(IntList(EOC, i487, o833))) → 1762_0_<init>_Load(EOS(STATIC_1762), java.lang.Object(IntList(EOC, i487, o833)))
1762_0_<init>_Load(EOS(STATIC_1762), java.lang.Object(IntList(EOC, i487, o833))) → 1766_0_<init>_Load(EOS(STATIC_1766), java.lang.Object(IntList(EOC, i487, o833)))
1766_0_<init>_Load(EOS(STATIC_1766), java.lang.Object(IntList(EOC, i487, o833))) → 1768_0_<init>_FieldAccess(EOS(STATIC_1768), java.lang.Object(IntList(EOC, i487, o833)))
1768_0_<init>_FieldAccess(EOS(STATIC_1768), java.lang.Object(IntList(EOC, i487, o833))) → 1771_0_<init>_Load(EOS(STATIC_1771), java.lang.Object(IntList(EOC, i487, o833)))
1771_0_<init>_Load(EOS(STATIC_1771), java.lang.Object(IntList(EOC, i487, o833))) → 1775_0_<init>_Load(EOS(STATIC_1775), java.lang.Object(IntList(EOC, i487, o833)))
1775_0_<init>_Load(EOS(STATIC_1775), java.lang.Object(IntList(EOC, i487, o833))) → 1779_0_<init>_FieldAccess(EOS(STATIC_1779), java.lang.Object(IntList(EOC, i487, o833)))
1779_0_<init>_FieldAccess(EOS(STATIC_1779), java.lang.Object(IntList(EOC, i487, o833))) → 1783_0_<init>_Return(EOS(STATIC_1783), java.lang.Object(IntList(EOC, i487, o833)))
1783_0_<init>_Return(EOS(STATIC_1783), java.lang.Object(IntList(EOC, i487, o833))) → 1787_0_reverse_Store(EOS(STATIC_1787), java.lang.Object(IntList(EOC, i487, o833)))
1787_0_reverse_Store(EOS(STATIC_1787), java.lang.Object(IntList(EOC, i487, o833))) → 1791_0_reverse_Load(EOS(STATIC_1791), java.lang.Object(IntList(EOC, i487, o833)))
1791_0_reverse_Load(EOS(STATIC_1791), java.lang.Object(IntList(EOC, i487, o833))) → 1794_0_reverse_FieldAccess(EOS(STATIC_1794), java.lang.Object(IntList(EOC, i487, o833)))
1794_0_reverse_FieldAccess(EOS(STATIC_1794), java.lang.Object(IntList(EOC, i487, o833))) → 1797_0_reverse_Store(EOS(STATIC_1797), o833)
1797_0_reverse_Store(EOS(STATIC_1797), o833) → 1800_0_reverse_JMP(EOS(STATIC_1800), o833)
1800_0_reverse_JMP(EOS(STATIC_1800), o833) → 1804_0_reverse_Load(EOS(STATIC_1804), o833)
1804_0_reverse_Load(EOS(STATIC_1804), o833) → 1713_0_reverse_Load(EOS(STATIC_1713), o833)
1713_0_reverse_Load(EOS(STATIC_1713), o818) → 1717_0_reverse_NULL(EOS(STATIC_1717), o818, o818)
1737_0_reverse_FieldAccess(EOS(STATIC_1737), java.lang.Object(IntList(EOC, i488, o835)), java.lang.Object(IntList(EOC, i488, o835))) → 1742_0_reverse_FieldAccess(EOS(STATIC_1742), java.lang.Object(IntList(EOC, i488, o835)), java.lang.Object(IntList(EOC, i488, o835)))
1742_0_reverse_FieldAccess(EOS(STATIC_1742), java.lang.Object(IntList(EOC, i488, o835)), java.lang.Object(IntList(EOC, i488, o835))) → 1747_0_reverse_Load(EOS(STATIC_1747), java.lang.Object(IntList(EOC, i488, o835)))
1747_0_reverse_Load(EOS(STATIC_1747), java.lang.Object(IntList(EOC, i488, o835))) → 1752_0_reverse_InvokeMethod(EOS(STATIC_1752), java.lang.Object(IntList(EOC, i488, o835)))
1752_0_reverse_InvokeMethod(EOS(STATIC_1752), java.lang.Object(IntList(EOC, i488, o835))) → 1757_0_<init>_Load(EOS(STATIC_1757), java.lang.Object(IntList(EOC, i488, o835)))
1757_0_<init>_Load(EOS(STATIC_1757), java.lang.Object(IntList(EOC, i488, o835))) → 1760_0_<init>_InvokeMethod(EOS(STATIC_1760), java.lang.Object(IntList(EOC, i488, o835)))
1760_0_<init>_InvokeMethod(EOS(STATIC_1760), java.lang.Object(IntList(EOC, i488, o835))) → 1764_0_<init>_Load(EOS(STATIC_1764), java.lang.Object(IntList(EOC, i488, o835)))
1764_0_<init>_Load(EOS(STATIC_1764), java.lang.Object(IntList(EOC, i488, o835))) → 1767_0_<init>_Load(EOS(STATIC_1767), java.lang.Object(IntList(EOC, i488, o835)))
1767_0_<init>_Load(EOS(STATIC_1767), java.lang.Object(IntList(EOC, i488, o835))) → 1770_0_<init>_FieldAccess(EOS(STATIC_1770), java.lang.Object(IntList(EOC, i488, o835)))
1770_0_<init>_FieldAccess(EOS(STATIC_1770), java.lang.Object(IntList(EOC, i488, o835))) → 1774_0_<init>_Load(EOS(STATIC_1774), java.lang.Object(IntList(EOC, i488, o835)))
1774_0_<init>_Load(EOS(STATIC_1774), java.lang.Object(IntList(EOC, i488, o835))) → 1777_0_<init>_Load(EOS(STATIC_1777), java.lang.Object(IntList(EOC, i488, o835)))
1777_0_<init>_Load(EOS(STATIC_1777), java.lang.Object(IntList(EOC, i488, o835))) → 1780_0_<init>_FieldAccess(EOS(STATIC_1780), java.lang.Object(IntList(EOC, i488, o835)))
1780_0_<init>_FieldAccess(EOS(STATIC_1780), java.lang.Object(IntList(EOC, i488, o835))) → 1786_0_<init>_Return(EOS(STATIC_1786), java.lang.Object(IntList(EOC, i488, o835)))
1786_0_<init>_Return(EOS(STATIC_1786), java.lang.Object(IntList(EOC, i488, o835))) → 1789_0_reverse_Store(EOS(STATIC_1789), java.lang.Object(IntList(EOC, i488, o835)))
1789_0_reverse_Store(EOS(STATIC_1789), java.lang.Object(IntList(EOC, i488, o835))) → 1792_0_reverse_Load(EOS(STATIC_1792), java.lang.Object(IntList(EOC, i488, o835)))
1792_0_reverse_Load(EOS(STATIC_1792), java.lang.Object(IntList(EOC, i488, o835))) → 1795_0_reverse_FieldAccess(EOS(STATIC_1795), java.lang.Object(IntList(EOC, i488, o835)))
1795_0_reverse_FieldAccess(EOS(STATIC_1795), java.lang.Object(IntList(EOC, i488, o835))) → 1799_0_reverse_Store(EOS(STATIC_1799), o835)
1799_0_reverse_Store(EOS(STATIC_1799), o835) → 1802_0_reverse_JMP(EOS(STATIC_1802), o835)
1802_0_reverse_JMP(EOS(STATIC_1802), o835) → 1807_0_reverse_Load(EOS(STATIC_1807), o835)
1807_0_reverse_Load(EOS(STATIC_1807), o835) → 1713_0_reverse_Load(EOS(STATIC_1713), o835)
R rules:

Combined rules. Obtained 1 conditional rules for P and 0 conditional rules for R.

P rules:
1717_0_reverse_NULL(EOS(STATIC_1717), java.lang.Object(IntList(EOC, x0, x1)), java.lang.Object(IntList(EOC, x0, x1))) → 1717_0_reverse_NULL(EOS(STATIC_1717), x1, x1)
R rules:

Filtered ground terms:

1717_0_reverse_NULL(x1, x2, x3) → 1717_0_reverse_NULL(x2, x3)
EOS(x1) → EOS
IntList(x1, x2, x3) → IntList(x2, x3)

Filtered duplicate args:

1717_0_reverse_NULL(x1, x2) → 1717_0_reverse_NULL(x2)

Filtered unneeded arguments:

IntList(x1, x2) → IntList(x2)

Combined rules. Obtained 1 conditional rules for P and 0 conditional rules for R.

P rules:
1717_0_reverse_NULL(java.lang.Object(IntList(x1))) → 1717_0_reverse_NULL(x1)
R rules:

Finished conversion. Obtained 1 rules for P and 0 rules for R. System has no predefined symbols.

P rules:
1717_0_REVERSE_NULL(java.lang.Object(IntList(x1))) → 1717_0_REVERSE_NULL(x1)
R rules:

(7) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:
none

R is empty.

The integer pair graph contains the following rules and edges:
(0): 1717_0_REVERSE_NULL(java.lang.Object(IntList(x1[0]))) → 1717_0_REVERSE_NULL(x1[0])

(0) -> (0), if (x1[0] →^* java.lang.Object(IntList(x1[0]')))

The set Q is empty.

(8) IDPtoQDPProof (SOUND transformation)

Represented integers and predefined function symbols by Terms

(9) Obligation:

Q DP problem:
The TRS P consists of the following rules:

1717_0_REVERSE_NULL(java.lang.Object(IntList(x1[0]))) → 1717_0_REVERSE_NULL(x1[0])

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(10) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

1717_0_REVERSE_NULL(java.lang.Object(IntList(x1[0]))) → 1717_0_REVERSE_NULL(x1[0])
The graph contains the following edges 1 > 1

(11) YES

(12) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: IntList.createIntList()LIntList;
SCC calls the following helper methods:
Performed SCC analyses: UsedFieldsAnalysis

(13) SCCToIDPv1Proof (SOUND transformation)

Transformed FIGraph SCCs to IDPs. Log:

Generated 40 rules for P and 0 rules for R.

P rules:
1425_0_createIntList_LE(EOS(STATIC_1425), i383, i383) → 1430_0_createIntList_LE(EOS(STATIC_1430), i383, i383)
1430_0_createIntList_LE(EOS(STATIC_1430), i383, i383) → 1434_0_createIntList_InvokeMethod(EOS(STATIC_1434), i383) | >(i383, 0)
1434_0_createIntList_InvokeMethod(EOS(STATIC_1434), i383) → 1437_0_random_FieldAccess(EOS(STATIC_1437), i383)
1437_0_random_FieldAccess(EOS(STATIC_1437), i383) → 1446_0_random_FieldAccess(EOS(STATIC_1446), i383)
1446_0_random_FieldAccess(EOS(STATIC_1446), i383) → 1452_0_random_ArrayAccess(EOS(STATIC_1452), i383)
1452_0_random_ArrayAccess(EOS(STATIC_1452), i383) → 1455_0_random_ArrayAccess(EOS(STATIC_1455), i383)
1455_0_random_ArrayAccess(EOS(STATIC_1455), i383) → 1459_0_random_Store(EOS(STATIC_1459), i383, o674)
1459_0_random_Store(EOS(STATIC_1459), i383, o674) → 1464_0_random_FieldAccess(EOS(STATIC_1464), i383, o674)
1464_0_random_FieldAccess(EOS(STATIC_1464), i383, o674) → 1467_0_random_ConstantStackPush(EOS(STATIC_1467), i383, o674)
1467_0_random_ConstantStackPush(EOS(STATIC_1467), i383, o674) → 1471_0_random_IntArithmetic(EOS(STATIC_1471), i383, o674)
1471_0_random_IntArithmetic(EOS(STATIC_1471), i383, o674) → 1476_0_random_FieldAccess(EOS(STATIC_1476), i383, o674)
1476_0_random_FieldAccess(EOS(STATIC_1476), i383, o674) → 1480_0_random_Load(EOS(STATIC_1480), i383, o674)
1480_0_random_Load(EOS(STATIC_1480), i383, o674) → 1488_0_random_InvokeMethod(EOS(STATIC_1488), i383, o674)
1488_0_random_InvokeMethod(EOS(STATIC_1488), i383, java.lang.Object(o692sub)) → 1493_0_random_InvokeMethod(EOS(STATIC_1493), i383, java.lang.Object(o692sub))
1493_0_random_InvokeMethod(EOS(STATIC_1493), i383, java.lang.Object(o692sub)) → 1498_0_length_Load(EOS(STATIC_1498), i383, java.lang.Object(o692sub), java.lang.Object(o692sub))
1498_0_length_Load(EOS(STATIC_1498), i383, java.lang.Object(o692sub), java.lang.Object(o692sub)) → 1510_0_length_FieldAccess(EOS(STATIC_1510), i383, java.lang.Object(o692sub), java.lang.Object(o692sub))
1510_0_length_FieldAccess(EOS(STATIC_1510), i383, java.lang.Object(java.lang.String(o700sub, i416)), java.lang.Object(java.lang.String(o700sub, i416))) → 1514_0_length_FieldAccess(EOS(STATIC_1514), i383, java.lang.Object(java.lang.String(o700sub, i416)), java.lang.Object(java.lang.String(o700sub, i416))) | &&(>=(i416, 0), >=(i417, 0))
1514_0_length_FieldAccess(EOS(STATIC_1514), i383, java.lang.Object(java.lang.String(o700sub, i416)), java.lang.Object(java.lang.String(o700sub, i416))) → 1522_0_length_Return(EOS(STATIC_1522), i383, java.lang.Object(java.lang.String(o700sub, i416)))
1522_0_length_Return(EOS(STATIC_1522), i383, java.lang.Object(java.lang.String(o700sub, i416))) → 1530_0_random_Return(EOS(STATIC_1530), i383)
1530_0_random_Return(EOS(STATIC_1530), i383) → 1536_0_createIntList_Store(EOS(STATIC_1536), i383)
1536_0_createIntList_Store(EOS(STATIC_1536), i383) → 1544_0_createIntList_New(EOS(STATIC_1544), i383)
1544_0_createIntList_New(EOS(STATIC_1544), i383) → 1551_0_createIntList_Duplicate(EOS(STATIC_1551), i383)
1551_0_createIntList_Duplicate(EOS(STATIC_1551), i383) → 1556_0_createIntList_Load(EOS(STATIC_1556), i383)
1556_0_createIntList_Load(EOS(STATIC_1556), i383) → 1563_0_createIntList_Load(EOS(STATIC_1563), i383)
1563_0_createIntList_Load(EOS(STATIC_1563), i383) → 1571_0_createIntList_InvokeMethod(EOS(STATIC_1571), i383)
1571_0_createIntList_InvokeMethod(EOS(STATIC_1571), i383) → 1576_0_<init>_Load(EOS(STATIC_1576), i383)
1576_0_<init>_Load(EOS(STATIC_1576), i383) → 1590_0_<init>_InvokeMethod(EOS(STATIC_1590), i383)
1590_0_<init>_InvokeMethod(EOS(STATIC_1590), i383) → 1598_0_<init>_Load(EOS(STATIC_1598), i383)
1598_0_<init>_Load(EOS(STATIC_1598), i383) → 1606_0_<init>_Load(EOS(STATIC_1606), i383)
1606_0_<init>_Load(EOS(STATIC_1606), i383) → 1615_0_<init>_FieldAccess(EOS(STATIC_1615), i383)
1615_0_<init>_FieldAccess(EOS(STATIC_1615), i383) → 1623_0_<init>_Load(EOS(STATIC_1623), i383)
1623_0_<init>_Load(EOS(STATIC_1623), i383) → 1631_0_<init>_Load(EOS(STATIC_1631), i383)
1631_0_<init>_Load(EOS(STATIC_1631), i383) → 1639_0_<init>_FieldAccess(EOS(STATIC_1639), i383)
1639_0_<init>_FieldAccess(EOS(STATIC_1639), i383) → 1646_0_<init>_Return(EOS(STATIC_1646), i383)
1646_0_<init>_Return(EOS(STATIC_1646), i383) → 1653_0_createIntList_Store(EOS(STATIC_1653), i383)
1653_0_createIntList_Store(EOS(STATIC_1653), i383) → 1661_0_createIntList_Inc(EOS(STATIC_1661), i383)
1661_0_createIntList_Inc(EOS(STATIC_1661), i383) → 1666_0_createIntList_JMP(EOS(STATIC_1666), +(i383, -1)) | >(i383, 0)
1666_0_createIntList_JMP(EOS(STATIC_1666), i472) → 1671_0_createIntList_Load(EOS(STATIC_1671), i472)
1671_0_createIntList_Load(EOS(STATIC_1671), i472) → 1420_0_createIntList_Load(EOS(STATIC_1420), i472)
1420_0_createIntList_Load(EOS(STATIC_1420), i378) → 1425_0_createIntList_LE(EOS(STATIC_1425), i378, i378)
R rules:

Combined rules. Obtained 1 conditional rules for P and 0 conditional rules for R.

P rules:
1425_0_createIntList_LE(EOS(STATIC_1425), x0, x0) → 1425_0_createIntList_LE(EOS(STATIC_1425), +(x0, -1), +(x0, -1)) | >(x0, 0)
R rules:

Filtered ground terms:

1425_0_createIntList_LE(x1, x2, x3) → 1425_0_createIntList_LE(x2, x3)
EOS(x1) → EOS
Cond_1425_0_createIntList_LE(x1, x2, x3, x4) → Cond_1425_0_createIntList_LE(x1, x3, x4)

Filtered duplicate args:

1425_0_createIntList_LE(x1, x2) → 1425_0_createIntList_LE(x2)
Cond_1425_0_createIntList_LE(x1, x2, x3) → Cond_1425_0_createIntList_LE(x1, x3)

Combined rules. Obtained 1 conditional rules for P and 0 conditional rules for R.

P rules:
1425_0_createIntList_LE(x0) → 1425_0_createIntList_LE(+(x0, -1)) | >(x0, 0)
R rules:

Finished conversion. Obtained 2 rules for P and 0 rules for R. System has predefined symbols.

P rules:
1425_0_CREATEINTLIST_LE(x0) → COND_1425_0_CREATEINTLIST_LE(>(x0, 0), x0)
COND_1425_0_CREATEINTLIST_LE(TRUE, x0) → 1425_0_CREATEINTLIST_LE(+(x0, -1))
R rules:

(14) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Integer

R is empty.

The integer pair graph contains the following rules and edges:
(0): 1425_0_CREATEINTLIST_LE(x0[0]) → COND_1425_0_CREATEINTLIST_LE(x0[0] > 0, x0[0])
(1): COND_1425_0_CREATEINTLIST_LE(TRUE, x0[1]) → 1425_0_CREATEINTLIST_LE(x0[1] + -1)

(0) -> (1), if (x0[0] > 0 ∧x0[0] →^* x0[1])

(1) -> (0), if (x0[1] + -1 →^* x0[0])

The set Q is empty.

(15) IDPNonInfProof (SOUND transformation)

Used the following options for this NonInfProof:
IDPGPoloSolver: Range: [(-1,2)] IsNat: false Interpretation Shape Heuristic: aprove.DPFramework.IDPProblem.Processors.nonInf.poly.IdpCand1ShapeHeuristic@229eb46b Constraint Generator: NonInfConstraintGenerator: PathGenerator: MetricPathGenerator: Max Left Steps: 0 Max Right Steps: 0

The constraints were generated the following way:
The DP Problem is simplified using the Induction Calculus [NONINF] with the following steps:
Note that final constraints are written in bold face.

For Pair 1425_0_CREATEINTLIST_LE(x0) → COND_1425_0_CREATEINTLIST_LE(>(x0, 0), x0) the following chains were created:

We consider the chain 1425_0_CREATEINTLIST_LE(x0[0]) → COND_1425_0_CREATEINTLIST_LE(>(x0[0], 0), x0[0]), COND_1425_0_CREATEINTLIST_LE(TRUE, x0[1]) → 1425_0_CREATEINTLIST_LE(+(x0[1], -1)) which results in the following constraint:
(1)    (>(x0[0], 0)=TRUE∧x0[0]=x0[1] ⇒ 1425_0_CREATEINTLIST_LE(x0[0])≥NonInfC∧1425_0_CREATEINTLIST_LE(x0[0])≥COND_1425_0_CREATEINTLIST_LE(>(x0[0], 0), x0[0])∧(U^Increasing(COND_1425_0_CREATEINTLIST_LE(>(x0[0], 0), x0[0])), ≥))

We simplified constraint (1) using rule (IV) which results in the following new constraint:
(2)    (>(x0[0], 0)=TRUE ⇒ 1425_0_CREATEINTLIST_LE(x0[0])≥NonInfC∧1425_0_CREATEINTLIST_LE(x0[0])≥COND_1425_0_CREATEINTLIST_LE(>(x0[0], 0), x0[0])∧(U^Increasing(COND_1425_0_CREATEINTLIST_LE(>(x0[0], 0), x0[0])), ≥))

We simplified constraint (2) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(3)    (x0[0] + [-1] ≥ 0 ⇒ (U^Increasing(COND_1425_0_CREATEINTLIST_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)

We simplified constraint (3) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(4)    (x0[0] + [-1] ≥ 0 ⇒ (U^Increasing(COND_1425_0_CREATEINTLIST_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)

We simplified constraint (4) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(5)    (x0[0] + [-1] ≥ 0 ⇒ (U^Increasing(COND_1425_0_CREATEINTLIST_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)

We simplified constraint (5) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(6)    (x0[0] ≥ 0 ⇒ (U^Increasing(COND_1425_0_CREATEINTLIST_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8 + (2)bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)

For Pair COND_1425_0_CREATEINTLIST_LE(TRUE, x0) → 1425_0_CREATEINTLIST_LE(+(x0, -1)) the following chains were created:

We consider the chain COND_1425_0_CREATEINTLIST_LE(TRUE, x0[1]) → 1425_0_CREATEINTLIST_LE(+(x0[1], -1)) which results in the following constraint:
(7)    (COND_1425_0_CREATEINTLIST_LE(TRUE, x0[1])≥NonInfC∧COND_1425_0_CREATEINTLIST_LE(TRUE, x0[1])≥1425_0_CREATEINTLIST_LE(+(x0[1], -1))∧(U^Increasing(1425_0_CREATEINTLIST_LE(+(x0[1], -1))), ≥))

We simplified constraint (7) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(8)    ((U^Increasing(1425_0_CREATEINTLIST_LE(+(x0[1], -1))), ≥)∧[bni_10] = 0∧[2 + (-1)bso_11] ≥ 0)

We simplified constraint (8) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(9)    ((U^Increasing(1425_0_CREATEINTLIST_LE(+(x0[1], -1))), ≥)∧[bni_10] = 0∧[2 + (-1)bso_11] ≥ 0)

We simplified constraint (9) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(10)    ((U^Increasing(1425_0_CREATEINTLIST_LE(+(x0[1], -1))), ≥)∧[bni_10] = 0∧[2 + (-1)bso_11] ≥ 0)

We simplified constraint (10) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(11)    ((U^Increasing(1425_0_CREATEINTLIST_LE(+(x0[1], -1))), ≥)∧[bni_10] = 0∧0 = 0∧[2 + (-1)bso_11] ≥ 0)

To summarize, we get the following constraints P_≥ for the following pairs.

1425_0_CREATEINTLIST_LE(x0) → COND_1425_0_CREATEINTLIST_LE(>(x0, 0), x0)
- (x0[0] ≥ 0 ⇒ (U^Increasing(COND_1425_0_CREATEINTLIST_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8 + (2)bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)
COND_1425_0_CREATEINTLIST_LE(TRUE, x0) → 1425_0_CREATEINTLIST_LE(+(x0, -1))
- ((U^Increasing(1425_0_CREATEINTLIST_LE(+(x0[1], -1))), ≥)∧[bni_10] = 0∧0 = 0∧[2 + (-1)bso_11] ≥ 0)

The constraints for P_> respective P_bound are constructed from P_≥ where we just replace every occurence of "t ≥ s" in P_≥ by "t > s" respective "t ≥ c". Here c stands for the fresh constant used for P_bound.
Using the following integer polynomial ordering the resulting constraints can be solved
Polynomial interpretation over integers[POLO]:

POL(TRUE) = 0
POL(FALSE) = 0
POL(1425_0_CREATEINTLIST_LE(x₁)) = [2]x₁
POL(COND_1425_0_CREATEINTLIST_LE(x₁, x₂)) = [2]x₂
POL(>(x₁, x₂)) = [-1]
POL(0) = 0
POL(+(x₁, x₂)) = x₁ + x₂
POL(-1) = [-1]

The following pairs are in P_>:

COND_1425_0_CREATEINTLIST_LE(TRUE, x0[1]) → 1425_0_CREATEINTLIST_LE(+(x0[1], -1))

The following pairs are in P_bound:

1425_0_CREATEINTLIST_LE(x0[0]) → COND_1425_0_CREATEINTLIST_LE(>(x0[0], 0), x0[0])

The following pairs are in P_≥:

1425_0_CREATEINTLIST_LE(x0[0]) → COND_1425_0_CREATEINTLIST_LE(>(x0[0], 0), x0[0])

There are no usable rules.

(16) Complex Obligation (AND)

(17) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Integer

R is empty.

The integer pair graph contains the following rules and edges:
(0): 1425_0_CREATEINTLIST_LE(x0[0]) → COND_1425_0_CREATEINTLIST_LE(x0[0] > 0, x0[0])

The set Q is empty.

(18) IDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.

(19) TRUE

(20) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Integer

R is empty.

The integer pair graph contains the following rules and edges:
(1): COND_1425_0_CREATEINTLIST_LE(TRUE, x0[1]) → 1425_0_CREATEINTLIST_LE(x0[1] + -1)

The set Q is empty.

(21) IDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.

(22) TRUE

(23) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: Shuffle.main([Ljava/lang/String;)V
SCC calls the following helper methods: IntList.reverse()LIntList;
Performed SCC analyses: UsedFieldsAnalysis

(24) SCCToIDPv1Proof (SOUND transformation)

Transformed FIGraph SCCs to IDPs. Log:

Generated 36 rules for P and 56 rules for R.

P rules:
1387_0_main_NULL(EOS(STATIC_1387), java.lang.Object(o648sub), o628, java.lang.Object(o648sub)) → 1398_0_main_NULL(EOS(STATIC_1398), java.lang.Object(o648sub), o628, java.lang.Object(o648sub))
1398_0_main_NULL(EOS(STATIC_1398), java.lang.Object(o648sub), o628, java.lang.Object(o648sub)) → 1407_0_main_New(EOS(STATIC_1407), java.lang.Object(o648sub), o628)
1407_0_main_New(EOS(STATIC_1407), java.lang.Object(o648sub), o628) → 1415_0_main_Duplicate(EOS(STATIC_1415), java.lang.Object(o648sub), o628, java.lang.Object(IntList(EOC, 0, NULL)))
1415_0_main_Duplicate(EOS(STATIC_1415), java.lang.Object(o648sub), o628, java.lang.Object(IntList(EOC, matching1, NULL))) → 1423_0_main_Load(EOS(STATIC_1423), java.lang.Object(o648sub), o628, java.lang.Object(IntList(EOC, 0, NULL)), java.lang.Object(IntList(EOC, 0, NULL))) | =(matching1, 0)
1423_0_main_Load(EOS(STATIC_1423), java.lang.Object(o648sub), o628, java.lang.Object(IntList(EOC, matching1, NULL)), java.lang.Object(IntList(EOC, matching2, NULL))) → 1427_0_main_FieldAccess(EOS(STATIC_1427), java.lang.Object(o648sub), o628, java.lang.Object(IntList(EOC, 0, NULL)), java.lang.Object(IntList(EOC, 0, NULL)), java.lang.Object(o648sub)) | &&(=(matching1, 0), =(matching2, 0))
1427_0_main_FieldAccess(EOS(STATIC_1427), java.lang.Object(IntList(EOC, i384, o665)), o628, java.lang.Object(IntList(EOC, matching1, NULL)), java.lang.Object(IntList(EOC, matching2, NULL)), java.lang.Object(IntList(EOC, i384, o665))) → 1432_0_main_FieldAccess(EOS(STATIC_1432), java.lang.Object(IntList(EOC, i384, o665)), o628, java.lang.Object(IntList(EOC, 0, NULL)), java.lang.Object(IntList(EOC, 0, NULL)), java.lang.Object(IntList(EOC, i384, o665))) | &&(=(matching1, 0), =(matching2, 0))
1432_0_main_FieldAccess(EOS(STATIC_1432), java.lang.Object(IntList(EOC, i384, o665)), o628, java.lang.Object(IntList(EOC, matching1, NULL)), java.lang.Object(IntList(EOC, matching2, NULL)), java.lang.Object(IntList(EOC, i384, o665))) → 1435_0_main_Load(EOS(STATIC_1435), java.lang.Object(IntList(EOC, i384, o665)), o628, java.lang.Object(IntList(EOC, 0, NULL)), java.lang.Object(IntList(EOC, 0, NULL)), i384) | &&(=(matching1, 0), =(matching2, 0))
1435_0_main_Load(EOS(STATIC_1435), java.lang.Object(IntList(EOC, i384, o665)), o628, java.lang.Object(IntList(EOC, matching1, NULL)), java.lang.Object(IntList(EOC, matching2, NULL)), i384) → 1439_0_main_InvokeMethod(EOS(STATIC_1439), java.lang.Object(IntList(EOC, i384, o665)), java.lang.Object(IntList(EOC, 0, NULL)), java.lang.Object(IntList(EOC, 0, NULL)), i384, o628) | &&(=(matching1, 0), =(matching2, 0))
1439_0_main_InvokeMethod(EOS(STATIC_1439), java.lang.Object(IntList(EOC, i384, o665)), java.lang.Object(IntList(EOC, matching1, NULL)), java.lang.Object(IntList(EOC, matching2, NULL)), i384, o628) → 1443_0_<init>_Load(EOS(STATIC_1443), java.lang.Object(IntList(EOC, i384, o665)), java.lang.Object(IntList(EOC, 0, NULL)), java.lang.Object(IntList(EOC, 0, NULL)), i384, o628, java.lang.Object(IntList(EOC, 0, NULL)), i384, o628) | &&(=(matching1, 0), =(matching2, 0))
1443_0_<init>_Load(EOS(STATIC_1443), java.lang.Object(IntList(EOC, i384, o665)), java.lang.Object(IntList(EOC, matching1, NULL)), java.lang.Object(IntList(EOC, matching2, NULL)), i384, o628, java.lang.Object(IntList(EOC, matching3, NULL)), i384, o628) → 1453_0_<init>_InvokeMethod(EOS(STATIC_1453), java.lang.Object(IntList(EOC, i384, o665)), java.lang.Object(IntList(EOC, 0, NULL)), java.lang.Object(IntList(EOC, 0, NULL)), i384, o628, java.lang.Object(IntList(EOC, 0, NULL)), i384, o628, java.lang.Object(IntList(EOC, 0, NULL))) | &&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0))
1453_0_<init>_InvokeMethod(EOS(STATIC_1453), java.lang.Object(IntList(EOC, i384, o665)), java.lang.Object(IntList(EOC, matching1, NULL)), java.lang.Object(IntList(EOC, matching2, NULL)), i384, o628, java.lang.Object(IntList(EOC, matching3, NULL)), i384, o628, java.lang.Object(IntList(EOC, matching4, NULL))) → 1458_0_<init>_Load(EOS(STATIC_1458), java.lang.Object(IntList(EOC, i384, o665)), java.lang.Object(IntList(EOC, 0, NULL)), java.lang.Object(IntList(EOC, 0, NULL)), i384, o628, java.lang.Object(IntList(EOC, 0, NULL)), i384, o628) | &&(&&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0)), =(matching4, 0))
1458_0_<init>_Load(EOS(STATIC_1458), java.lang.Object(IntList(EOC, i384, o665)), java.lang.Object(IntList(EOC, matching1, NULL)), java.lang.Object(IntList(EOC, matching2, NULL)), i384, o628, java.lang.Object(IntList(EOC, matching3, NULL)), i384, o628) → 1462_0_<init>_Load(EOS(STATIC_1462), java.lang.Object(IntList(EOC, i384, o665)), java.lang.Object(IntList(EOC, 0, NULL)), java.lang.Object(IntList(EOC, 0, NULL)), i384, o628, java.lang.Object(IntList(EOC, 0, NULL)), i384, o628, java.lang.Object(IntList(EOC, 0, NULL))) | &&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0))
1462_0_<init>_Load(EOS(STATIC_1462), java.lang.Object(IntList(EOC, i384, o665)), java.lang.Object(IntList(EOC, matching1, NULL)), java.lang.Object(IntList(EOC, matching2, NULL)), i384, o628, java.lang.Object(IntList(EOC, matching3, NULL)), i384, o628, java.lang.Object(IntList(EOC, matching4, NULL))) → 1465_0_<init>_FieldAccess(EOS(STATIC_1465), java.lang.Object(IntList(EOC, i384, o665)), java.lang.Object(IntList(EOC, 0, NULL)), java.lang.Object(IntList(EOC, 0, NULL)), i384, o628, java.lang.Object(IntList(EOC, 0, NULL)), o628, java.lang.Object(IntList(EOC, 0, NULL)), i384) | &&(&&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0)), =(matching4, 0))
1465_0_<init>_FieldAccess(EOS(STATIC_1465), java.lang.Object(IntList(EOC, i384, o665)), java.lang.Object(IntList(EOC, matching1, NULL)), java.lang.Object(IntList(EOC, matching2, NULL)), i384, o628, java.lang.Object(IntList(EOC, matching3, NULL)), o628, java.lang.Object(IntList(EOC, matching4, NULL)), i384) → 1470_0_<init>_Load(EOS(STATIC_1470), java.lang.Object(IntList(EOC, i384, o665)), java.lang.Object(IntList(EOC, i384, NULL)), java.lang.Object(IntList(EOC, i384, NULL)), i384, o628, java.lang.Object(IntList(EOC, i384, NULL)), o628) | &&(&&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0)), =(matching4, 0))
1470_0_<init>_Load(EOS(STATIC_1470), java.lang.Object(IntList(EOC, i384, o665)), java.lang.Object(IntList(EOC, i384, NULL)), java.lang.Object(IntList(EOC, i384, NULL)), i384, o628, java.lang.Object(IntList(EOC, i384, NULL)), o628) → 1474_0_<init>_Load(EOS(STATIC_1474), java.lang.Object(IntList(EOC, i384, o665)), java.lang.Object(IntList(EOC, i384, NULL)), java.lang.Object(IntList(EOC, i384, NULL)), i384, o628, o628, java.lang.Object(IntList(EOC, i384, NULL)))
1474_0_<init>_Load(EOS(STATIC_1474), java.lang.Object(IntList(EOC, i384, o665)), java.lang.Object(IntList(EOC, i384, NULL)), java.lang.Object(IntList(EOC, i384, NULL)), i384, o628, o628, java.lang.Object(IntList(EOC, i384, NULL))) → 1478_0_<init>_FieldAccess(EOS(STATIC_1478), java.lang.Object(IntList(EOC, i384, o665)), java.lang.Object(IntList(EOC, i384, NULL)), java.lang.Object(IntList(EOC, i384, NULL)), i384, o628, java.lang.Object(IntList(EOC, i384, NULL)), o628)
1478_0_<init>_FieldAccess(EOS(STATIC_1478), java.lang.Object(IntList(EOC, i384, o665)), java.lang.Object(IntList(EOC, i384, NULL)), java.lang.Object(IntList(EOC, i384, NULL)), i384, o628, java.lang.Object(IntList(EOC, i384, NULL)), o628) → 1484_0_<init>_Return(EOS(STATIC_1484), java.lang.Object(IntList(EOC, i384, o665)), java.lang.Object(IntList(EOC, i384, o628)), java.lang.Object(IntList(EOC, i384, o628)), i384, o628)
1484_0_<init>_Return(EOS(STATIC_1484), java.lang.Object(IntList(EOC, i384, o665)), java.lang.Object(IntList(EOC, i384, o628)), java.lang.Object(IntList(EOC, i384, o628)), i384, o628) → 1491_0_main_Store(EOS(STATIC_1491), java.lang.Object(IntList(EOC, i384, o665)), java.lang.Object(IntList(EOC, i384, o628)))
1491_0_main_Store(EOS(STATIC_1491), java.lang.Object(IntList(EOC, i384, o665)), java.lang.Object(IntList(EOC, i384, o628))) → 1496_0_main_Load(EOS(STATIC_1496), java.lang.Object(IntList(EOC, i384, o665)), java.lang.Object(IntList(EOC, i384, o628)))
1496_0_main_Load(EOS(STATIC_1496), java.lang.Object(IntList(EOC, i384, o665)), java.lang.Object(IntList(EOC, i384, o628))) → 1503_0_main_FieldAccess(EOS(STATIC_1503), java.lang.Object(IntList(EOC, i384, o628)), java.lang.Object(IntList(EOC, i384, o665)))
1503_0_main_FieldAccess(EOS(STATIC_1503), java.lang.Object(IntList(EOC, i384, o628)), java.lang.Object(IntList(EOC, i384, o665))) → 1508_0_main_Store(EOS(STATIC_1508), java.lang.Object(IntList(EOC, i384, o628)), o665)
1508_0_main_Store(EOS(STATIC_1508), java.lang.Object(IntList(EOC, i384, o628)), o665) → 1512_0_main_Load(EOS(STATIC_1512), o665, java.lang.Object(IntList(EOC, i384, o628)))
1512_0_main_Load(EOS(STATIC_1512), o665, java.lang.Object(IntList(EOC, i384, o628))) → 1520_0_main_NULL(EOS(STATIC_1520), o665, java.lang.Object(IntList(EOC, i384, o628)), o665)
1520_0_main_NULL(EOS(STATIC_1520), java.lang.Object(o706sub), java.lang.Object(IntList(EOC, i384, o628)), java.lang.Object(o706sub)) → 1527_0_main_NULL(EOS(STATIC_1527), java.lang.Object(o706sub), java.lang.Object(IntList(EOC, i384, o628)), java.lang.Object(o706sub))
1520_0_main_NULL(EOS(STATIC_1520), NULL, java.lang.Object(IntList(EOC, i384, o628)), NULL) → 1528_0_main_NULL(EOS(STATIC_1528), NULL, java.lang.Object(IntList(EOC, i384, o628)), NULL)
1527_0_main_NULL(EOS(STATIC_1527), java.lang.Object(o706sub), java.lang.Object(IntList(EOC, i384, o628)), java.lang.Object(o706sub)) → 1532_0_main_Load(EOS(STATIC_1532), java.lang.Object(o706sub), java.lang.Object(IntList(EOC, i384, o628)))
1532_0_main_Load(EOS(STATIC_1532), java.lang.Object(o706sub), java.lang.Object(IntList(EOC, i384, o628))) → 1542_0_main_InvokeMethod(EOS(STATIC_1542), java.lang.Object(IntList(EOC, i384, o628)), java.lang.Object(o706sub))
1542_0_main_InvokeMethod(EOS(STATIC_1542), java.lang.Object(IntList(EOC, i384, o628)), java.lang.Object(o706sub)) → 1549_1_main_InvokeMethod(1549_0_reverse_ConstantStackPush(EOS(STATIC_1549), java.lang.Object(o706sub)), java.lang.Object(IntList(EOC, i384, o628)), java.lang.Object(o706sub))
1549_1_main_InvokeMethod(1726_0_reverse_Return(EOS(STATIC_1726), o817), java.lang.Object(IntList(EOC, i384, o628)), java.lang.Object(o830sub)) → 1738_0_reverse_Return(EOS(STATIC_1738), java.lang.Object(IntList(EOC, i384, o628)), java.lang.Object(o830sub), o817)
1738_0_reverse_Return(EOS(STATIC_1738), java.lang.Object(IntList(EOC, i384, o628)), java.lang.Object(o830sub), o817) → 1743_0_main_Store(EOS(STATIC_1743), java.lang.Object(IntList(EOC, i384, o628)), o817)
1743_0_main_Store(EOS(STATIC_1743), java.lang.Object(IntList(EOC, i384, o628)), o817) → 1748_0_main_JMP(EOS(STATIC_1748), o817, java.lang.Object(IntList(EOC, i384, o628)))
1748_0_main_JMP(EOS(STATIC_1748), o817, java.lang.Object(IntList(EOC, i384, o628))) → 1753_0_main_Load(EOS(STATIC_1753), o817, java.lang.Object(IntList(EOC, i384, o628)))
1753_0_main_Load(EOS(STATIC_1753), o817, java.lang.Object(IntList(EOC, i384, o628))) → 1380_0_main_Load(EOS(STATIC_1380), o817, java.lang.Object(IntList(EOC, i384, o628)))
1380_0_main_Load(EOS(STATIC_1380), o627, o628) → 1387_0_main_NULL(EOS(STATIC_1387), o627, o628, o627)
1528_0_main_NULL(EOS(STATIC_1528), NULL, java.lang.Object(IntList(EOC, i384, o628)), NULL) → 1534_0_main_Load(EOS(STATIC_1534), NULL, java.lang.Object(IntList(EOC, i384, o628)))
1534_0_main_Load(EOS(STATIC_1534), NULL, java.lang.Object(IntList(EOC, i384, o628))) → 1380_0_main_Load(EOS(STATIC_1380), NULL, java.lang.Object(IntList(EOC, i384, o628)))
R rules:
1549_0_reverse_ConstantStackPush(EOS(STATIC_1549), java.lang.Object(o706sub)) → 1555_0_reverse_ConstantStackPush(EOS(STATIC_1555), java.lang.Object(o706sub))
1555_0_reverse_ConstantStackPush(EOS(STATIC_1555), java.lang.Object(o706sub)) → 1569_0_reverse_ConstantStackPush(EOS(STATIC_1569), java.lang.Object(o706sub))
1569_0_reverse_ConstantStackPush(EOS(STATIC_1569), java.lang.Object(o706sub)) → 1575_0_reverse_Store(EOS(STATIC_1575), java.lang.Object(o706sub), NULL)
1575_0_reverse_Store(EOS(STATIC_1575), java.lang.Object(o706sub), NULL) → 1582_0_reverse_Load(EOS(STATIC_1582), java.lang.Object(o706sub), NULL)
1582_0_reverse_Load(EOS(STATIC_1582), java.lang.Object(o706sub), NULL) → 1589_0_reverse_Store(EOS(STATIC_1589), NULL, java.lang.Object(o706sub))
1589_0_reverse_Store(EOS(STATIC_1589), NULL, java.lang.Object(o706sub)) → 1597_0_reverse_Load(EOS(STATIC_1597), NULL, java.lang.Object(o706sub))
1597_0_reverse_Load(EOS(STATIC_1597), NULL, java.lang.Object(o706sub)) → 1713_0_reverse_Load(EOS(STATIC_1713), NULL, java.lang.Object(o706sub))
1713_0_reverse_Load(EOS(STATIC_1713), o817, o818) → 1717_0_reverse_NULL(EOS(STATIC_1717), o817, o818, o818)
1717_0_reverse_NULL(EOS(STATIC_1717), o817, java.lang.Object(o828sub), java.lang.Object(o828sub)) → 1719_0_reverse_NULL(EOS(STATIC_1719), o817, java.lang.Object(o828sub), java.lang.Object(o828sub))
1717_0_reverse_NULL(EOS(STATIC_1717), o817, NULL, NULL) → 1720_0_reverse_NULL(EOS(STATIC_1720), o817, NULL, NULL)
1719_0_reverse_NULL(EOS(STATIC_1719), o817, java.lang.Object(o828sub), java.lang.Object(o828sub)) → 1721_0_reverse_New(EOS(STATIC_1721), o817, java.lang.Object(o828sub))
1720_0_reverse_NULL(EOS(STATIC_1720), o817, NULL, NULL) → 1723_0_reverse_Load(EOS(STATIC_1723), o817)
1721_0_reverse_New(EOS(STATIC_1721), o817, java.lang.Object(o828sub)) → 1725_0_reverse_Duplicate(EOS(STATIC_1725), o817, java.lang.Object(o828sub), java.lang.Object(IntList(EOC, 0, NULL)))
1723_0_reverse_Load(EOS(STATIC_1723), o817) → 1726_0_reverse_Return(EOS(STATIC_1726), o817)
1725_0_reverse_Duplicate(EOS(STATIC_1725), o817, java.lang.Object(o828sub), java.lang.Object(IntList(EOC, matching1, NULL))) → 1728_0_reverse_Load(EOS(STATIC_1728), o817, java.lang.Object(o828sub), java.lang.Object(IntList(EOC, 0, NULL)), java.lang.Object(IntList(EOC, 0, NULL))) | =(matching1, 0)
1728_0_reverse_Load(EOS(STATIC_1728), o817, java.lang.Object(o828sub), java.lang.Object(IntList(EOC, matching1, NULL)), java.lang.Object(IntList(EOC, matching2, NULL))) → 1731_0_reverse_FieldAccess(EOS(STATIC_1731), o817, java.lang.Object(o828sub), java.lang.Object(IntList(EOC, 0, NULL)), java.lang.Object(IntList(EOC, 0, NULL)), java.lang.Object(o828sub)) | &&(=(matching1, 0), =(matching2, 0))
1731_0_reverse_FieldAccess(EOS(STATIC_1731), o817, java.lang.Object(o828sub), java.lang.Object(IntList(EOC, matching1, NULL)), java.lang.Object(IntList(EOC, matching2, NULL)), java.lang.Object(o828sub)) → 1736_0_reverse_FieldAccess(EOS(STATIC_1736), o817, java.lang.Object(o828sub), java.lang.Object(IntList(EOC, 0, NULL)), java.lang.Object(IntList(EOC, 0, NULL)), java.lang.Object(o828sub)) | &&(=(matching1, 0), =(matching2, 0))
1731_0_reverse_FieldAccess(EOS(STATIC_1731), o817, java.lang.Object(o815sub), java.lang.Object(IntList(EOC, matching1, NULL)), java.lang.Object(IntList(EOC, matching2, NULL)), java.lang.Object(o815sub)) → 1737_0_reverse_FieldAccess(EOS(STATIC_1737), o817, java.lang.Object(o815sub), java.lang.Object(IntList(EOC, 0, NULL)), java.lang.Object(IntList(EOC, 0, NULL)), java.lang.Object(o815sub)) | &&(=(matching1, 0), =(matching2, 0))
1736_0_reverse_FieldAccess(EOS(STATIC_1736), o817, java.lang.Object(IntList(EOC, i487, o833)), java.lang.Object(IntList(EOC, matching1, NULL)), java.lang.Object(IntList(EOC, matching2, NULL)), java.lang.Object(IntList(EOC, i487, o833))) → 1740_0_reverse_FieldAccess(EOS(STATIC_1740), o817, java.lang.Object(IntList(EOC, i487, o833)), java.lang.Object(IntList(EOC, 0, NULL)), java.lang.Object(IntList(EOC, 0, NULL)), java.lang.Object(IntList(EOC, i487, o833))) | &&(=(matching1, 0), =(matching2, 0))
1737_0_reverse_FieldAccess(EOS(STATIC_1737), o817, java.lang.Object(IntList(EOC, i488, o835)), java.lang.Object(IntList(EOC, matching1, NULL)), java.lang.Object(IntList(EOC, matching2, NULL)), java.lang.Object(IntList(EOC, i488, o835))) → 1742_0_reverse_FieldAccess(EOS(STATIC_1742), o817, java.lang.Object(IntList(EOC, i488, o835)), java.lang.Object(IntList(EOC, 0, NULL)), java.lang.Object(IntList(EOC, 0, NULL)), java.lang.Object(IntList(EOC, i488, o835))) | &&(=(matching1, 0), =(matching2, 0))
1740_0_reverse_FieldAccess(EOS(STATIC_1740), o817, java.lang.Object(IntList(EOC, i487, o833)), java.lang.Object(IntList(EOC, matching1, NULL)), java.lang.Object(IntList(EOC, matching2, NULL)), java.lang.Object(IntList(EOC, i487, o833))) → 1745_0_reverse_Load(EOS(STATIC_1745), o817, java.lang.Object(IntList(EOC, i487, o833)), java.lang.Object(IntList(EOC, 0, NULL)), java.lang.Object(IntList(EOC, 0, NULL)), i487) | &&(=(matching1, 0), =(matching2, 0))
1742_0_reverse_FieldAccess(EOS(STATIC_1742), o817, java.lang.Object(IntList(EOC, i488, o835)), java.lang.Object(IntList(EOC, matching1, NULL)), java.lang.Object(IntList(EOC, matching2, NULL)), java.lang.Object(IntList(EOC, i488, o835))) → 1747_0_reverse_Load(EOS(STATIC_1747), o817, java.lang.Object(IntList(EOC, i488, o835)), java.lang.Object(IntList(EOC, 0, NULL)), java.lang.Object(IntList(EOC, 0, NULL)), i488) | &&(=(matching1, 0), =(matching2, 0))
1745_0_reverse_Load(EOS(STATIC_1745), o817, java.lang.Object(IntList(EOC, i487, o833)), java.lang.Object(IntList(EOC, matching1, NULL)), java.lang.Object(IntList(EOC, matching2, NULL)), i487) → 1750_0_reverse_InvokeMethod(EOS(STATIC_1750), java.lang.Object(IntList(EOC, i487, o833)), java.lang.Object(IntList(EOC, 0, NULL)), java.lang.Object(IntList(EOC, 0, NULL)), i487, o817) | &&(=(matching1, 0), =(matching2, 0))
1747_0_reverse_Load(EOS(STATIC_1747), o817, java.lang.Object(IntList(EOC, i488, o835)), java.lang.Object(IntList(EOC, matching1, NULL)), java.lang.Object(IntList(EOC, matching2, NULL)), i488) → 1752_0_reverse_InvokeMethod(EOS(STATIC_1752), java.lang.Object(IntList(EOC, i488, o835)), java.lang.Object(IntList(EOC, 0, NULL)), java.lang.Object(IntList(EOC, 0, NULL)), i488, o817) | &&(=(matching1, 0), =(matching2, 0))
1750_0_reverse_InvokeMethod(EOS(STATIC_1750), java.lang.Object(IntList(EOC, i487, o833)), java.lang.Object(IntList(EOC, matching1, NULL)), java.lang.Object(IntList(EOC, matching2, NULL)), i487, o817) → 1755_0_<init>_Load(EOS(STATIC_1755), java.lang.Object(IntList(EOC, i487, o833)), java.lang.Object(IntList(EOC, 0, NULL)), java.lang.Object(IntList(EOC, 0, NULL)), i487, o817, java.lang.Object(IntList(EOC, 0, NULL)), i487, o817) | &&(=(matching1, 0), =(matching2, 0))
1752_0_reverse_InvokeMethod(EOS(STATIC_1752), java.lang.Object(IntList(EOC, i488, o835)), java.lang.Object(IntList(EOC, matching1, NULL)), java.lang.Object(IntList(EOC, matching2, NULL)), i488, o817) → 1757_0_<init>_Load(EOS(STATIC_1757), java.lang.Object(IntList(EOC, i488, o835)), java.lang.Object(IntList(EOC, 0, NULL)), java.lang.Object(IntList(EOC, 0, NULL)), i488, o817, java.lang.Object(IntList(EOC, 0, NULL)), i488, o817) | &&(=(matching1, 0), =(matching2, 0))
1755_0_<init>_Load(EOS(STATIC_1755), java.lang.Object(IntList(EOC, i487, o833)), java.lang.Object(IntList(EOC, matching1, NULL)), java.lang.Object(IntList(EOC, matching2, NULL)), i487, o817, java.lang.Object(IntList(EOC, matching3, NULL)), i487, o817) → 1758_0_<init>_InvokeMethod(EOS(STATIC_1758), java.lang.Object(IntList(EOC, i487, o833)), java.lang.Object(IntList(EOC, 0, NULL)), java.lang.Object(IntList(EOC, 0, NULL)), i487, o817, java.lang.Object(IntList(EOC, 0, NULL)), i487, o817, java.lang.Object(IntList(EOC, 0, NULL))) | &&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0))
1757_0_<init>_Load(EOS(STATIC_1757), java.lang.Object(IntList(EOC, i488, o835)), java.lang.Object(IntList(EOC, matching1, NULL)), java.lang.Object(IntList(EOC, matching2, NULL)), i488, o817, java.lang.Object(IntList(EOC, matching3, NULL)), i488, o817) → 1760_0_<init>_InvokeMethod(EOS(STATIC_1760), java.lang.Object(IntList(EOC, i488, o835)), java.lang.Object(IntList(EOC, 0, NULL)), java.lang.Object(IntList(EOC, 0, NULL)), i488, o817, java.lang.Object(IntList(EOC, 0, NULL)), i488, o817, java.lang.Object(IntList(EOC, 0, NULL))) | &&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0))
1758_0_<init>_InvokeMethod(EOS(STATIC_1758), java.lang.Object(IntList(EOC, i487, o833)), java.lang.Object(IntList(EOC, matching1, NULL)), java.lang.Object(IntList(EOC, matching2, NULL)), i487, o817, java.lang.Object(IntList(EOC, matching3, NULL)), i487, o817, java.lang.Object(IntList(EOC, matching4, NULL))) → 1762_0_<init>_Load(EOS(STATIC_1762), java.lang.Object(IntList(EOC, i487, o833)), java.lang.Object(IntList(EOC, 0, NULL)), java.lang.Object(IntList(EOC, 0, NULL)), i487, o817, java.lang.Object(IntList(EOC, 0, NULL)), i487, o817) | &&(&&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0)), =(matching4, 0))
1760_0_<init>_InvokeMethod(EOS(STATIC_1760), java.lang.Object(IntList(EOC, i488, o835)), java.lang.Object(IntList(EOC, matching1, NULL)), java.lang.Object(IntList(EOC, matching2, NULL)), i488, o817, java.lang.Object(IntList(EOC, matching3, NULL)), i488, o817, java.lang.Object(IntList(EOC, matching4, NULL))) → 1764_0_<init>_Load(EOS(STATIC_1764), java.lang.Object(IntList(EOC, i488, o835)), java.lang.Object(IntList(EOC, 0, NULL)), java.lang.Object(IntList(EOC, 0, NULL)), i488, o817, java.lang.Object(IntList(EOC, 0, NULL)), i488, o817) | &&(&&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0)), =(matching4, 0))
1762_0_<init>_Load(EOS(STATIC_1762), java.lang.Object(IntList(EOC, i487, o833)), java.lang.Object(IntList(EOC, matching1, NULL)), java.lang.Object(IntList(EOC, matching2, NULL)), i487, o817, java.lang.Object(IntList(EOC, matching3, NULL)), i487, o817) → 1766_0_<init>_Load(EOS(STATIC_1766), java.lang.Object(IntList(EOC, i487, o833)), java.lang.Object(IntList(EOC, 0, NULL)), java.lang.Object(IntList(EOC, 0, NULL)), i487, o817, java.lang.Object(IntList(EOC, 0, NULL)), i487, o817, java.lang.Object(IntList(EOC, 0, NULL))) | &&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0))
1764_0_<init>_Load(EOS(STATIC_1764), java.lang.Object(IntList(EOC, i488, o835)), java.lang.Object(IntList(EOC, matching1, NULL)), java.lang.Object(IntList(EOC, matching2, NULL)), i488, o817, java.lang.Object(IntList(EOC, matching3, NULL)), i488, o817) → 1767_0_<init>_Load(EOS(STATIC_1767), java.lang.Object(IntList(EOC, i488, o835)), java.lang.Object(IntList(EOC, 0, NULL)), java.lang.Object(IntList(EOC, 0, NULL)), i488, o817, java.lang.Object(IntList(EOC, 0, NULL)), i488, o817, java.lang.Object(IntList(EOC, 0, NULL))) | &&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0))
1766_0_<init>_Load(EOS(STATIC_1766), java.lang.Object(IntList(EOC, i487, o833)), java.lang.Object(IntList(EOC, matching1, NULL)), java.lang.Object(IntList(EOC, matching2, NULL)), i487, o817, java.lang.Object(IntList(EOC, matching3, NULL)), i487, o817, java.lang.Object(IntList(EOC, matching4, NULL))) → 1768_0_<init>_FieldAccess(EOS(STATIC_1768), java.lang.Object(IntList(EOC, i487, o833)), java.lang.Object(IntList(EOC, 0, NULL)), java.lang.Object(IntList(EOC, 0, NULL)), i487, o817, java.lang.Object(IntList(EOC, 0, NULL)), o817, java.lang.Object(IntList(EOC, 0, NULL)), i487) | &&(&&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0)), =(matching4, 0))
1767_0_<init>_Load(EOS(STATIC_1767), java.lang.Object(IntList(EOC, i488, o835)), java.lang.Object(IntList(EOC, matching1, NULL)), java.lang.Object(IntList(EOC, matching2, NULL)), i488, o817, java.lang.Object(IntList(EOC, matching3, NULL)), i488, o817, java.lang.Object(IntList(EOC, matching4, NULL))) → 1770_0_<init>_FieldAccess(EOS(STATIC_1770), java.lang.Object(IntList(EOC, i488, o835)), java.lang.Object(IntList(EOC, 0, NULL)), java.lang.Object(IntList(EOC, 0, NULL)), i488, o817, java.lang.Object(IntList(EOC, 0, NULL)), o817, java.lang.Object(IntList(EOC, 0, NULL)), i488) | &&(&&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0)), =(matching4, 0))
1768_0_<init>_FieldAccess(EOS(STATIC_1768), java.lang.Object(IntList(EOC, i487, o833)), java.lang.Object(IntList(EOC, matching1, NULL)), java.lang.Object(IntList(EOC, matching2, NULL)), i487, o817, java.lang.Object(IntList(EOC, matching3, NULL)), o817, java.lang.Object(IntList(EOC, matching4, NULL)), i487) → 1771_0_<init>_Load(EOS(STATIC_1771), java.lang.Object(IntList(EOC, i487, o833)), java.lang.Object(IntList(EOC, i487, NULL)), java.lang.Object(IntList(EOC, i487, NULL)), i487, o817, java.lang.Object(IntList(EOC, i487, NULL)), o817) | &&(&&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0)), =(matching4, 0))
1770_0_<init>_FieldAccess(EOS(STATIC_1770), java.lang.Object(IntList(EOC, i488, o835)), java.lang.Object(IntList(EOC, matching1, NULL)), java.lang.Object(IntList(EOC, matching2, NULL)), i488, o817, java.lang.Object(IntList(EOC, matching3, NULL)), o817, java.lang.Object(IntList(EOC, matching4, NULL)), i488) → 1774_0_<init>_Load(EOS(STATIC_1774), java.lang.Object(IntList(EOC, i488, o835)), java.lang.Object(IntList(EOC, i488, NULL)), java.lang.Object(IntList(EOC, i488, NULL)), i488, o817, java.lang.Object(IntList(EOC, i488, NULL)), o817) | &&(&&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0)), =(matching4, 0))
1771_0_<init>_Load(EOS(STATIC_1771), java.lang.Object(IntList(EOC, i487, o833)), java.lang.Object(IntList(EOC, i487, NULL)), java.lang.Object(IntList(EOC, i487, NULL)), i487, o817, java.lang.Object(IntList(EOC, i487, NULL)), o817) → 1775_0_<init>_Load(EOS(STATIC_1775), java.lang.Object(IntList(EOC, i487, o833)), java.lang.Object(IntList(EOC, i487, NULL)), java.lang.Object(IntList(EOC, i487, NULL)), i487, o817, o817, java.lang.Object(IntList(EOC, i487, NULL)))
1774_0_<init>_Load(EOS(STATIC_1774), java.lang.Object(IntList(EOC, i488, o835)), java.lang.Object(IntList(EOC, i488, NULL)), java.lang.Object(IntList(EOC, i488, NULL)), i488, o817, java.lang.Object(IntList(EOC, i488, NULL)), o817) → 1777_0_<init>_Load(EOS(STATIC_1777), java.lang.Object(IntList(EOC, i488, o835)), java.lang.Object(IntList(EOC, i488, NULL)), java.lang.Object(IntList(EOC, i488, NULL)), i488, o817, o817, java.lang.Object(IntList(EOC, i488, NULL)))
1775_0_<init>_Load(EOS(STATIC_1775), java.lang.Object(IntList(EOC, i487, o833)), java.lang.Object(IntList(EOC, i487, NULL)), java.lang.Object(IntList(EOC, i487, NULL)), i487, o817, o817, java.lang.Object(IntList(EOC, i487, NULL))) → 1779_0_<init>_FieldAccess(EOS(STATIC_1779), java.lang.Object(IntList(EOC, i487, o833)), java.lang.Object(IntList(EOC, i487, NULL)), java.lang.Object(IntList(EOC, i487, NULL)), i487, o817, java.lang.Object(IntList(EOC, i487, NULL)), o817)
1777_0_<init>_Load(EOS(STATIC_1777), java.lang.Object(IntList(EOC, i488, o835)), java.lang.Object(IntList(EOC, i488, NULL)), java.lang.Object(IntList(EOC, i488, NULL)), i488, o817, o817, java.lang.Object(IntList(EOC, i488, NULL))) → 1780_0_<init>_FieldAccess(EOS(STATIC_1780), java.lang.Object(IntList(EOC, i488, o835)), java.lang.Object(IntList(EOC, i488, NULL)), java.lang.Object(IntList(EOC, i488, NULL)), i488, o817, java.lang.Object(IntList(EOC, i488, NULL)), o817)
1779_0_<init>_FieldAccess(EOS(STATIC_1779), java.lang.Object(IntList(EOC, i487, o833)), java.lang.Object(IntList(EOC, i487, NULL)), java.lang.Object(IntList(EOC, i487, NULL)), i487, o817, java.lang.Object(IntList(EOC, i487, NULL)), o817) → 1783_0_<init>_Return(EOS(STATIC_1783), java.lang.Object(IntList(EOC, i487, o833)), java.lang.Object(IntList(EOC, i487, o817)), java.lang.Object(IntList(EOC, i487, o817)), i487, o817)
1780_0_<init>_FieldAccess(EOS(STATIC_1780), java.lang.Object(IntList(EOC, i488, o835)), java.lang.Object(IntList(EOC, i488, NULL)), java.lang.Object(IntList(EOC, i488, NULL)), i488, o817, java.lang.Object(IntList(EOC, i488, NULL)), o817) → 1786_0_<init>_Return(EOS(STATIC_1786), java.lang.Object(IntList(EOC, i488, o835)), java.lang.Object(IntList(EOC, i488, o817)), java.lang.Object(IntList(EOC, i488, o817)), i488, o817)
1783_0_<init>_Return(EOS(STATIC_1783), java.lang.Object(IntList(EOC, i487, o833)), java.lang.Object(IntList(EOC, i487, o817)), java.lang.Object(IntList(EOC, i487, o817)), i487, o817) → 1787_0_reverse_Store(EOS(STATIC_1787), java.lang.Object(IntList(EOC, i487, o833)), java.lang.Object(IntList(EOC, i487, o817)))
1786_0_<init>_Return(EOS(STATIC_1786), java.lang.Object(IntList(EOC, i488, o835)), java.lang.Object(IntList(EOC, i488, o817)), java.lang.Object(IntList(EOC, i488, o817)), i488, o817) → 1789_0_reverse_Store(EOS(STATIC_1789), java.lang.Object(IntList(EOC, i488, o835)), java.lang.Object(IntList(EOC, i488, o817)))
1787_0_reverse_Store(EOS(STATIC_1787), java.lang.Object(IntList(EOC, i487, o833)), java.lang.Object(IntList(EOC, i487, o817))) → 1791_0_reverse_Load(EOS(STATIC_1791), java.lang.Object(IntList(EOC, i487, o817)), java.lang.Object(IntList(EOC, i487, o833)))
1789_0_reverse_Store(EOS(STATIC_1789), java.lang.Object(IntList(EOC, i488, o835)), java.lang.Object(IntList(EOC, i488, o817))) → 1792_0_reverse_Load(EOS(STATIC_1792), java.lang.Object(IntList(EOC, i488, o817)), java.lang.Object(IntList(EOC, i488, o835)))
1791_0_reverse_Load(EOS(STATIC_1791), java.lang.Object(IntList(EOC, i487, o817)), java.lang.Object(IntList(EOC, i487, o833))) → 1794_0_reverse_FieldAccess(EOS(STATIC_1794), java.lang.Object(IntList(EOC, i487, o817)), java.lang.Object(IntList(EOC, i487, o833)))
1792_0_reverse_Load(EOS(STATIC_1792), java.lang.Object(IntList(EOC, i488, o817)), java.lang.Object(IntList(EOC, i488, o835))) → 1795_0_reverse_FieldAccess(EOS(STATIC_1795), java.lang.Object(IntList(EOC, i488, o817)), java.lang.Object(IntList(EOC, i488, o835)))
1794_0_reverse_FieldAccess(EOS(STATIC_1794), java.lang.Object(IntList(EOC, i487, o817)), java.lang.Object(IntList(EOC, i487, o833))) → 1797_0_reverse_Store(EOS(STATIC_1797), java.lang.Object(IntList(EOC, i487, o817)), o833)
1795_0_reverse_FieldAccess(EOS(STATIC_1795), java.lang.Object(IntList(EOC, i488, o817)), java.lang.Object(IntList(EOC, i488, o835))) → 1799_0_reverse_Store(EOS(STATIC_1799), java.lang.Object(IntList(EOC, i488, o817)), o835)
1797_0_reverse_Store(EOS(STATIC_1797), java.lang.Object(IntList(EOC, i487, o817)), o833) → 1800_0_reverse_JMP(EOS(STATIC_1800), java.lang.Object(IntList(EOC, i487, o817)), o833)
1799_0_reverse_Store(EOS(STATIC_1799), java.lang.Object(IntList(EOC, i488, o817)), o835) → 1802_0_reverse_JMP(EOS(STATIC_1802), java.lang.Object(IntList(EOC, i488, o817)), o835)
1800_0_reverse_JMP(EOS(STATIC_1800), java.lang.Object(IntList(EOC, i487, o817)), o833) → 1804_0_reverse_Load(EOS(STATIC_1804), java.lang.Object(IntList(EOC, i487, o817)), o833)
1802_0_reverse_JMP(EOS(STATIC_1802), java.lang.Object(IntList(EOC, i488, o817)), o835) → 1807_0_reverse_Load(EOS(STATIC_1807), java.lang.Object(IntList(EOC, i488, o817)), o835)
1804_0_reverse_Load(EOS(STATIC_1804), java.lang.Object(IntList(EOC, i487, o817)), o833) → 1713_0_reverse_Load(EOS(STATIC_1713), java.lang.Object(IntList(EOC, i487, o817)), o833)
1807_0_reverse_Load(EOS(STATIC_1807), java.lang.Object(IntList(EOC, i488, o817)), o835) → 1713_0_reverse_Load(EOS(STATIC_1713), java.lang.Object(IntList(EOC, i488, o817)), o835)

Combined rules. Obtained 3 conditional rules for P and 3 conditional rules for R.

P rules:
1387_0_main_NULL(EOS(STATIC_1387), java.lang.Object(IntList(EOC, x0, java.lang.Object(x1))), x2, java.lang.Object(IntList(EOC, x0, java.lang.Object(x1)))) → 1549_1_main_InvokeMethod(1549_0_reverse_ConstantStackPush(EOS(STATIC_1549), java.lang.Object(x1)), java.lang.Object(IntList(EOC, x0, x2)), java.lang.Object(x1))
1549_1_main_InvokeMethod(1726_0_reverse_Return(EOS(STATIC_1726), x0), java.lang.Object(IntList(EOC, x1, x2)), java.lang.Object(x3)) → 1387_0_main_NULL(EOS(STATIC_1387), x0, java.lang.Object(IntList(EOC, x1, x2)), x0)
1387_0_main_NULL(EOS(STATIC_1387), java.lang.Object(IntList(EOC, x0, NULL)), x1, java.lang.Object(IntList(EOC, x0, NULL))) → 1387_0_main_NULL(EOS(STATIC_1387), NULL, java.lang.Object(IntList(EOC, x0, x1)), NULL)
R rules:
1549_0_reverse_ConstantStackPush(EOS(STATIC_1549), java.lang.Object(x0)) → 1717_0_reverse_NULL(EOS(STATIC_1717), NULL, java.lang.Object(x0), java.lang.Object(x0))
1717_0_reverse_NULL(EOS(STATIC_1717), x0, NULL, NULL) → 1726_0_reverse_Return(EOS(STATIC_1726), x0)
1717_0_reverse_NULL(EOS(STATIC_1717), x0, java.lang.Object(IntList(EOC, x1, x2)), java.lang.Object(IntList(EOC, x1, x2))) → 1717_0_reverse_NULL(EOS(STATIC_1717), java.lang.Object(IntList(EOC, x1, x0)), x2, x2)

Filtered ground terms:

1387_0_main_NULL(x1, x2, x3, x4) → 1387_0_main_NULL(x2, x3, x4)
IntList(x1, x2, x3) → IntList(x2, x3)
1726_0_reverse_Return(x1, x2) → 1726_0_reverse_Return(x2)
1549_0_reverse_ConstantStackPush(x1, x2) → 1549_0_reverse_ConstantStackPush(x2)
1717_0_reverse_NULL(x1, x2, x3, x4) → 1717_0_reverse_NULL(x2, x3, x4)

Filtered duplicate args:

1387_0_main_NULL(x1, x2, x3) → 1387_0_main_NULL(x2, x3)
1717_0_reverse_NULL(x1, x2, x3) → 1717_0_reverse_NULL(x1, x3)

Filtered unneeded arguments:

1387_0_main_NULL(x1, x2) → 1387_0_main_NULL(x2)
IntList(x1, x2) → IntList(x2)
1549_1_main_InvokeMethod(x1, x2, x3) → 1549_1_main_InvokeMethod(x1)

Combined rules. Obtained 3 conditional rules for P and 3 conditional rules for R.

P rules:
1387_0_main_NULL(java.lang.Object(IntList(java.lang.Object(x1)))) → 1549_1_main_InvokeMethod(1549_0_reverse_ConstantStackPush(java.lang.Object(x1)))
1549_1_main_InvokeMethod(1726_0_reverse_Return(x0)) → 1387_0_main_NULL(x0)
1387_0_main_NULL(java.lang.Object(IntList(NULL))) → 1387_0_main_NULL(NULL)
R rules:
1549_0_reverse_ConstantStackPush(java.lang.Object(x0)) → 1717_0_reverse_NULL(NULL, java.lang.Object(x0))
1717_0_reverse_NULL(x0, NULL) → 1726_0_reverse_Return(x0)
1717_0_reverse_NULL(x0, java.lang.Object(IntList(x2))) → 1717_0_reverse_NULL(java.lang.Object(IntList(x0)), x2)

Finished conversion. Obtained 3 rules for P and 3 rules for R. System has no predefined symbols.

P rules:
1387_0_MAIN_NULL(java.lang.Object(IntList(java.lang.Object(x1)))) → 1549_1_MAIN_INVOKEMETHOD(1549_0_reverse_ConstantStackPush(java.lang.Object(x1)))
1549_1_MAIN_INVOKEMETHOD(1726_0_reverse_Return(x0)) → 1387_0_MAIN_NULL(x0)
1387_0_MAIN_NULL(java.lang.Object(IntList(NULL))) → 1387_0_MAIN_NULL(NULL)
R rules:
1549_0_reverse_ConstantStackPush(java.lang.Object(x0)) → 1717_0_reverse_NULL(NULL, java.lang.Object(x0))
1717_0_reverse_NULL(x0, NULL) → 1726_0_reverse_Return(x0)
1717_0_reverse_NULL(x0, java.lang.Object(IntList(x2))) → 1717_0_reverse_NULL(java.lang.Object(IntList(x0)), x2)

(25) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:
none

The ITRS R consists of the following rules:
1549_0_reverse_ConstantStackPush(java.lang.Object(x0)) → 1717_0_reverse_NULL(NULL, java.lang.Object(x0))
1717_0_reverse_NULL(x0, NULL) → 1726_0_reverse_Return(x0)
1717_0_reverse_NULL(x0, java.lang.Object(IntList(x2))) → 1717_0_reverse_NULL(java.lang.Object(IntList(x0)), x2)

The integer pair graph contains the following rules and edges:
(0): 1387_0_MAIN_NULL(java.lang.Object(IntList(java.lang.Object(x1[0])))) → 1549_1_MAIN_INVOKEMETHOD(1549_0_reverse_ConstantStackPush(java.lang.Object(x1[0])))
(1): 1549_1_MAIN_INVOKEMETHOD(1726_0_reverse_Return(x0[1])) → 1387_0_MAIN_NULL(x0[1])
(2): 1387_0_MAIN_NULL(java.lang.Object(IntList(NULL))) → 1387_0_MAIN_NULL(NULL)

(0) -> (1), if (1549_0_reverse_ConstantStackPush(java.lang.Object(x1[0])) →^* 1726_0_reverse_Return(x0[1]))

(1) -> (0), if (x0[1] →^* java.lang.Object(IntList(java.lang.Object(x1[0]))))

(1) -> (2), if (x0[1] →^* java.lang.Object(IntList(NULL)))

(2) -> (0), if (NULL →^* java.lang.Object(IntList(java.lang.Object(x1[0]))))

(2) -> (2), if (NULL →^* java.lang.Object(IntList(NULL)))

The set Q consists of the following terms:
1549_0_reverse_ConstantStackPush(java.lang.Object(x0))
1717_0_reverse_NULL(x0, NULL)
1717_0_reverse_NULL(x0, java.lang.Object(IntList(x1)))

(26) IDPtoQDPProof (SOUND transformation)

Represented integers and predefined function symbols by Terms

(27) Obligation:

Q DP problem:
The TRS P consists of the following rules:

1387_0_MAIN_NULL(java.lang.Object(IntList(java.lang.Object(x1[0])))) → 1549_1_MAIN_INVOKEMETHOD(1549_0_reverse_ConstantStackPush(java.lang.Object(x1[0])))
1549_1_MAIN_INVOKEMETHOD(1726_0_reverse_Return(x0[1])) → 1387_0_MAIN_NULL(x0[1])
1387_0_MAIN_NULL(java.lang.Object(IntList(NULL))) → 1387_0_MAIN_NULL(NULL)

The TRS R consists of the following rules:

1549_0_reverse_ConstantStackPush(java.lang.Object(x0)) → 1717_0_reverse_NULL(NULL, java.lang.Object(x0))
1717_0_reverse_NULL(x0, NULL) → 1726_0_reverse_Return(x0)
1717_0_reverse_NULL(x0, java.lang.Object(IntList(x2))) → 1717_0_reverse_NULL(java.lang.Object(IntList(x0)), x2)

The set Q consists of the following terms:

1549_0_reverse_ConstantStackPush(java.lang.Object(x0))
1717_0_reverse_NULL(x0, NULL)
1717_0_reverse_NULL(x0, java.lang.Object(IntList(x1)))

We have to consider all minimal (P,Q,R)-chains.

(28) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

(29) Obligation:

Q DP problem:
The TRS P consists of the following rules:

1549_1_MAIN_INVOKEMETHOD(1726_0_reverse_Return(x0[1])) → 1387_0_MAIN_NULL(x0[1])
1387_0_MAIN_NULL(java.lang.Object(IntList(java.lang.Object(x1[0])))) → 1549_1_MAIN_INVOKEMETHOD(1549_0_reverse_ConstantStackPush(java.lang.Object(x1[0])))

The TRS R consists of the following rules:

1549_0_reverse_ConstantStackPush(java.lang.Object(x0)) → 1717_0_reverse_NULL(NULL, java.lang.Object(x0))
1717_0_reverse_NULL(x0, NULL) → 1726_0_reverse_Return(x0)
1717_0_reverse_NULL(x0, java.lang.Object(IntList(x2))) → 1717_0_reverse_NULL(java.lang.Object(IntList(x0)), x2)

The set Q consists of the following terms:

1549_0_reverse_ConstantStackPush(java.lang.Object(x0))
1717_0_reverse_NULL(x0, NULL)
1717_0_reverse_NULL(x0, java.lang.Object(IntList(x1)))

We have to consider all minimal (P,Q,R)-chains.

(30) MRRProof (EQUIVALENT transformation)

By using the rule removal processor [LPAR04] with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.

Strictly oriented rules of the TRS R:

1549_0_reverse_ConstantStackPush(java.lang.Object(x0)) → 1717_0_reverse_NULL(NULL, java.lang.Object(x0))

Used ordering: Polynomial interpretation [POLO]:

POL(1387_0_MAIN_NULL(x₁)) = 2·x₁
POL(1549_0_reverse_ConstantStackPush(x₁)) = 2 + x₁
POL(1549_1_MAIN_INVOKEMETHOD(x₁)) = 2·x₁
POL(1717_0_reverse_NULL(x₁, x₂)) = x₁ + x₂
POL(1726_0_reverse_Return(x₁)) = x₁
POL(IntList(x₁)) = 2 + x₁
POL(NULL) = 0
POL(java.lang.Object(x₁)) = x₁

(31) Obligation:

Q DP problem:
The TRS P consists of the following rules:

1549_1_MAIN_INVOKEMETHOD(1726_0_reverse_Return(x0[1])) → 1387_0_MAIN_NULL(x0[1])
1387_0_MAIN_NULL(java.lang.Object(IntList(java.lang.Object(x1[0])))) → 1549_1_MAIN_INVOKEMETHOD(1549_0_reverse_ConstantStackPush(java.lang.Object(x1[0])))

The TRS R consists of the following rules:

1717_0_reverse_NULL(x0, NULL) → 1726_0_reverse_Return(x0)
1717_0_reverse_NULL(x0, java.lang.Object(IntList(x2))) → 1717_0_reverse_NULL(java.lang.Object(IntList(x0)), x2)

The set Q consists of the following terms:

1549_0_reverse_ConstantStackPush(java.lang.Object(x0))
1717_0_reverse_NULL(x0, NULL)
1717_0_reverse_NULL(x0, java.lang.Object(IntList(x1)))

We have to consider all minimal (P,Q,R)-chains.

(32) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 2 less nodes.

(0) Obligation:

(1) JBCToGraph (SOUND transformation)

(2) Obligation:

(3) TerminationGraphToSCCProof (SOUND transformation)

(4) Complex Obligation (AND)

(5) Obligation:

(6) SCCToIDPv1Proof (SOUND transformation)

(7) Obligation:

(8) IDPtoQDPProof (SOUND transformation)

(9) Obligation:

(10) QDPSizeChangeProof (EQUIVALENT transformation)

(11) YES

(12) Obligation:

(13) SCCToIDPv1Proof (SOUND transformation)

(14) Obligation:

(15) IDPNonInfProof (SOUND transformation)

(16) Complex Obligation (AND)

(17) Obligation:

(18) IDependencyGraphProof (EQUIVALENT transformation)

(19) TRUE

(20) Obligation:

(21) IDependencyGraphProof (EQUIVALENT transformation)

(22) TRUE

(23) Obligation:

(24) SCCToIDPv1Proof (SOUND transformation)

(25) Obligation:

(26) IDPtoQDPProof (SOUND transformation)

(27) Obligation:

(28) DependencyGraphProof (EQUIVALENT transformation)

(29) Obligation:

(30) MRRProof (EQUIVALENT transformation)

(31) Obligation:

(32) DependencyGraphProof (EQUIVALENT transformation)

(33) TRUE